ing hilite.me --><div style="background: #ffffff; overflow:auto;width:auto;border:solid gray;border-width:.1em .1em .1em .8em;padding:.2em .6em;"><table><tr><td><pre style="margin: 0; line-height: 125%">  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105</pre></td><td><pre style="margin: 0; line-height: 125%"><span style="color: #008800; font-weight: bold">from</span> <span style="color: #0e84b5; font-weight: bold">z3</span> <span style="color: #008800; font-weight: bold">import</span> <span style="color: #333333">*</span>

<span style="color: #008800; font-weight: bold">import</span> <span style="color: #0e84b5; font-weight: bold">time</span>
<span style="color: #008800; font-weight: bold">import</span> <span style="color: #0e84b5; font-weight: bold">random</span>

<span style="color: #008800; font-weight: bold">def</span> <span style="color: #0066BB; font-weight: bold">flat</span>(unflat):
    flat_dict <span style="color: #333333">=</span> []
    <span style="color: #008800; font-weight: bold">for</span> sublist <span style="color: #000000; font-weight: bold">in</span> unflat:
        <span style="color: #008800; font-weight: bold">for</span> item <span style="color: #000000; font-weight: bold">in</span> sublist:
            flat_dict<span style="color: #333333">.</span>append(item)
    <span style="color: #008800; font-weight: bold">return</span> flat_dict

<span style="color: #008800; font-weight: bold">def</span> <span style="color: #0066BB; font-weight: bold">attack_graph</span>():

    t <span style="color: #333333">=</span> time<span style="color: #333333">.</span>time()

    n_size, unroll, base <span style="color: #333333">=</span> <span style="color: #0000DD; font-weight: bold">5</span>, <span style="color: #0000DD; font-weight: bold">3</span>, <span style="color: #0000DD; font-weight: bold">1</span>

    s         <span style="color: #333333">=</span> Solver()
    node      <span style="color: #333333">=</span> []
    edge_list <span style="color: #333333">=</span> []

    unflat <span style="color: #333333">=</span> [ BitVecs(<span style="background-color: #fff0f0">&#39;node_id_</span><span style="background-color: #eeeeee">%d</span><span style="background-color: #fff0f0">&#39;</span> <span style="color: #333333">%</span> (i), <span style="color: #0000DD; font-weight: bold">4</span>) <span style="color: #008800; font-weight: bold">for</span> i <span style="color: #000000; font-weight: bold">in</span> <span style="color: #007020">range</span>(n_size)]
    node_id <span style="color: #333333">=</span> flat(unflat)

    unflat <span style="color: #333333">=</span> [ BitVecs(<span style="background-color: #fff0f0">&#39;node_type_</span><span style="background-color: #eeeeee">%d</span><span style="background-color: #fff0f0">&#39;</span> <span style="color: #333333">%</span> (i), <span style="color: #0000DD; font-weight: bold">3</span>) <span style="color: #008800; font-weight: bold">for</span> i <span style="color: #000000; font-weight: bold">in</span> <span style="color: #007020">range</span>(n_size)]
    node_type <span style="color: #333333">=</span> flat(unflat)

    unflat <span style="color: #333333">=</span> [ Bools(<span style="background-color: #fff0f0">&#39;node_safe_</span><span style="background-color: #eeeeee">%d</span><span style="background-color: #fff0f0">&#39;</span> <span style="color: #333333">%</span> (i)) <span style="color: #008800; font-weight: bold">for</span> i <span style="color: #000000; font-weight: bold">in</span> <span style="color: #007020">range</span>(n_size)]
    node_safe <span style="color: #333333">=</span> flat(unflat)
    
    unflat <span style="color: #333333">=</span> [ BitVecs(<span style="background-color: #fff0f0">&#39;node_domain_</span><span style="background-color: #eeeeee">%d</span><span style="background-color: #fff0f0">&#39;</span> <span style="color: #333333">%</span> (i), <span style="color: #0000DD; font-weight: bold">2</span>) <span style="color: #008800; font-weight: bold">for</span> i <span style="color: #000000; font-weight: bold">in</span> <span style="color: #007020">range</span>(n_size)]
    node_domain <span style="color: #333333">=</span> flat(unflat)
    
    <span style="color: #007020">tuple</span> <span style="color: #333333">=</span> z3<span style="color: #333333">.</span>Datatype(<span style="background-color: #fff0f0">&#39;tuple&#39;</span>)
    <span style="color: #007020">tuple</span><span style="color: #333333">.</span>declare(<span style="background-color: #fff0f0">&#39;tuple&#39;</span>,(<span style="background-color: #fff0f0">&#39;f1&#39;</span>, BitVecSort(<span style="color: #0000DD; font-weight: bold">4</span>)), (<span style="background-color: #fff0f0">&#39;f2&#39;</span>, BitVecSort(<span style="color: #0000DD; font-weight: bold">3</span>)), (<span style="background-color: #fff0f0">&#39;f3&#39;</span>, BoolSort()), (<span style="background-color: #fff0f0">&#39;f4&#39;</span>, BitVecSort(<span style="color: #0000DD; font-weight: bold">2</span>)))
    <span style="color: #007020">tuple</span> <span style="color: #333333">=</span> <span style="color: #007020">tuple</span><span style="color: #333333">.</span>create()

    edge <span style="color: #333333">=</span> z3<span style="color: #333333">.</span>Datatype(<span style="background-color: #fff0f0">&#39;edge&#39;</span>)
    edge<span style="color: #333333">.</span>declare(<span style="background-color: #fff0f0">&#39;edge&#39;</span>,(<span style="background-color: #fff0f0">&#39;f1&#39;</span>, <span style="color: #007020">tuple</span>), (<span style="background-color: #fff0f0">&#39;f2&#39;</span>, <span style="color: #007020">tuple</span>))
    edge <span style="color: #333333">=</span> edge<span style="color: #333333">.</span>create()
    
    <span style="color: #008800; font-weight: bold">for</span> i <span style="color: #000000; font-weight: bold">in</span> <span style="color: #007020">range</span>(unroll<span style="color: #333333">+</span>base):
        node<span style="color: #333333">.</span>append([<span style="color: #007020">tuple</span><span style="color: #333333">.</span>tuple(node_id[i], node_type[i], node_safe[i], node_domain[i]) <span style="color: #008800; font-weight: bold">for</span> i <span style="color: #000000; font-weight: bold">in</span> <span style="color: #007020">range</span>(n_size)])    

    node[<span style="color: #0000DD; font-weight: bold">0</span>][<span style="color: #0000DD; font-weight: bold">0</span>]  <span style="color: #333333">=</span> <span style="color: #007020">tuple</span><span style="color: #333333">.</span>tuple(<span style="color: #0000DD; font-weight: bold">0</span>, <span style="color: #0000DD; font-weight: bold">0</span>, <span style="color: #007020">True</span>, <span style="color: #0000DD; font-weight: bold">0</span>)
    node[<span style="color: #0000DD; font-weight: bold">0</span>][<span style="color: #0000DD; font-weight: bold">1</span>]  <span style="color: #333333">=</span> <span style="color: #007020">tuple</span><span style="color: #333333">.</span>tuple(<span style="color: #0000DD; font-weight: bold">1</span>, <span style="color: #0000DD; font-weight: bold">0</span>, <span style="color: #007020">False</span>, <span style="color: #0000DD; font-weight: bold">0</span>) 
    node[<span style="color: #0000DD; font-weight: bold">0</span>][<span style="color: #0000DD; font-weight: bold">2</span>]  <span style="color: #333333">=</span> <span style="color: #007020">tuple</span><span style="color: #333333">.</span>tuple(<span style="color: #0000DD; font-weight: bold">2</span>, <span style="color: #0000DD; font-weight: bold">0</span>, <span style="color: #007020">True</span>, <span style="color: #0000DD; font-weight: bold">0</span>)
    node[<span style="color: #0000DD; font-weight: bold">0</span>][<span style="color: #0000DD; font-weight: bold">3</span>]  <span style="color: #333333">=</span> <span style="color: #007020">tuple</span><span style="color: #333333">.</span>tuple(<span style="color: #0000DD; font-weight: bold">3</span>, <span style="color: #0000DD; font-weight: bold">0</span>, <span style="color: #007020">True</span>, <span style="color: #0000DD; font-weight: bold">0</span>) 
    node[<span style="color: #0000DD; font-weight: bold">0</span>][<span style="color: #0000DD; font-weight: bold">4</span>]  <span style="color: #333333">=</span> <span style="color: #007020">tuple</span><span style="color: #333333">.</span>tuple(<span style="color: #0000DD; font-weight: bold">4</span>, <span style="color: #0000DD; font-weight: bold">0</span>, <span style="color: #007020">True</span>, <span style="color: #0000DD; font-weight: bold">2</span>)

    edge_list<span style="color: #333333">.</span>append(edge<span style="color: #333333">.</span>edge(node[<span style="color: #0000DD; font-weight: bold">0</span>][<span style="color: #0000DD; font-weight: bold">0</span>],  node[<span style="color: #0000DD; font-weight: bold">0</span>][<span style="color: #0000DD; font-weight: bold">1</span>]))
    edge_list<span style="color: #333333">.</span>append(edge<span style="color: #333333">.</span>edge(node[<span style="color: #0000DD; font-weight: bold">0</span>][<span style="color: #0000DD; font-weight: bold">1</span>],  node[<span style="color: #0000DD; font-weight: bold">0</span>][<span style="color: #0000DD; font-weight: bold">2</span>]))
    edge_list<span style="color: #333333">.</span>append(edge<span style="color: #333333">.</span>edge(node[<span style="color: #0000DD; font-weight: bold">0</span>][<span style="color: #0000DD; font-weight: bold">2</span>],  node[<span style="color: #0000DD; font-weight: bold">0</span>][<span style="color: #0000DD; font-weight: bold">3</span>]))
    edge_list<span style="color: #333333">.</span>append(edge<span style="color: #333333">.</span>edge(node[<span style="color: #0000DD; font-weight: bold">0</span>][<span style="color: #0000DD; font-weight: bold">3</span>],  node[<span style="color: #0000DD; font-weight: bold">0</span>][<span style="color: #0000DD; font-weight: bold">4</span>]))

    a <span style="color: #333333">=</span> z3<span style="color: #333333">.</span>K(edge, <span style="color: #007020">False</span>)

    <span style="color: #008800; font-weight: bold">for</span> i <span style="color: #000000; font-weight: bold">in</span> <span style="color: #007020">range</span>(<span style="color: #007020">len</span>(edge_list)):
        a <span style="color: #333333">=</span> z3<span style="color: #333333">.</span>Store(a, edge_list[i], <span style="color: #007020">True</span>)

    <span style="color: #008800; font-weight: bold">for</span> u <span style="color: #000000; font-weight: bold">in</span> <span style="color: #007020">range</span>(<span style="color: #0000DD; font-weight: bold">1</span>, unroll<span style="color: #333333">+</span>base):

        equal <span style="color: #333333">=</span> []
        <span style="color: #008800; font-weight: bold">for</span> i <span style="color: #000000; font-weight: bold">in</span> <span style="color: #007020">range</span>(n_size):
            equal_pr1 <span style="color: #333333">=</span> And( <span style="color: #007020">tuple</span><span style="color: #333333">.</span>f1(node[u<span style="color: #333333">-</span><span style="color: #0000DD; font-weight: bold">1</span>][i]) <span style="color: #333333">==</span> <span style="color: #007020">tuple</span><span style="color: #333333">.</span>f1(node[u][i])) 
            equal_pr2 <span style="color: #333333">=</span> And( <span style="color: #007020">tuple</span><span style="color: #333333">.</span>f2(node[u<span style="color: #333333">-</span><span style="color: #0000DD; font-weight: bold">1</span>][i]) <span style="color: #333333">==</span> <span style="color: #007020">tuple</span><span style="color: #333333">.</span>f2(node[u][i]))
            equal_pr4 <span style="color: #333333">=</span> And( <span style="color: #007020">tuple</span><span style="color: #333333">.</span>f4(node[u<span style="color: #333333">-</span><span style="color: #0000DD; font-weight: bold">1</span>][i]) <span style="color: #333333">==</span> <span style="color: #007020">tuple</span><span style="color: #333333">.</span>f4(node[u][i]))
            equal<span style="color: #333333">.</span>extend([equal_pr1, equal_pr2, equal_pr4])
        s<span style="color: #333333">.</span>add(<span style="color: #333333">*</span>equal)

        <span style="color: #008800; font-weight: bold">for</span> i <span style="color: #000000; font-weight: bold">in</span> <span style="color: #007020">range</span>(n_size):
            invariant <span style="color: #333333">=</span> []
            <span style="color: #008800; font-weight: bold">for</span> j <span style="color: #000000; font-weight: bold">in</span> <span style="color: #007020">range</span>(n_size):
                is_edge_exist          <span style="color: #333333">=</span>  (Select(a, edge<span style="color: #333333">.</span>edge(node[<span style="color: #0000DD; font-weight: bold">0</span>][i], node[<span style="color: #0000DD; font-weight: bold">0</span>][j])) <span style="color: #333333">==</span> <span style="color: #007020">True</span>)
                is_curr_node_unsafe    <span style="color: #333333">=</span>  (<span style="color: #007020">tuple</span><span style="color: #333333">.</span>f3(node[u<span style="color: #333333">-</span><span style="color: #0000DD; font-weight: bold">1</span>][i]) <span style="color: #333333">==</span> <span style="color: #007020">False</span>)
                make_next_node_unsafe  <span style="color: #333333">=</span>  (<span style="color: #007020">tuple</span><span style="color: #333333">.</span>f3(node[u][j])   <span style="color: #333333">==</span> <span style="color: #007020">False</span>)        
                invariant<span style="color: #333333">.</span>append(Implies(And(is_edge_exist, is_curr_node_unsafe), make_next_node_unsafe))
            s<span style="color: #333333">.</span>add(And(<span style="color: #333333">*</span>invariant))
        
        equal_3 <span style="color: #333333">=</span> []
        <span style="color: #008800; font-weight: bold">for</span> i <span style="color: #000000; font-weight: bold">in</span> <span style="color: #007020">range</span>(n_size):
            equal_pr3 <span style="color: #333333">=</span> Implies(Not(<span style="color: #007020">tuple</span><span style="color: #333333">.</span>f3(node[u][i]) <span style="color: #333333">==</span> <span style="color: #007020">False</span>), <span style="color: #007020">tuple</span><span style="color: #333333">.</span>f3(node[u<span style="color: #333333">-</span><span style="color: #0000DD; font-weight: bold">1</span>][i]) <span style="color: #333333">==</span> <span style="color: #007020">tuple</span><span style="color: #333333">.</span>f3(node[u][i])) 
            equal_3<span style="color: #333333">.</span>extend([equal_pr3])
        s<span style="color: #333333">.</span>add(<span style="color: #333333">*</span>equal_3)
        
        safety <span style="color: #333333">=</span> []
        <span style="color: #008800; font-weight: bold">for</span> i <span style="color: #000000; font-weight: bold">in</span> <span style="color: #007020">range</span>(n_size):
            safety<span style="color: #333333">.</span>append(Implies(<span style="color: #007020">tuple</span><span style="color: #333333">.</span>f4(node[u][i]) <span style="color: #333333">==</span> <span style="color: #0000DD; font-weight: bold">2</span>, <span style="color: #007020">tuple</span><span style="color: #333333">.</span>f3(node[u][i]) <span style="color: #333333">==</span> <span style="color: #007020">True</span>))
        <span style="color: #888888">#s.add(*safety)</span>
            
        x <span style="color: #333333">=</span> s<span style="color: #333333">.</span>check()
        <span style="color: #008800; font-weight: bold">print</span>(<span style="background-color: #fff0f0">&quot;</span><span style="color: #666666; font-weight: bold; background-color: #fff0f0">\n</span><span style="background-color: #fff0f0">unroll : &quot;</span>, u)
        <span style="color: #008800; font-weight: bold">print</span>(x)
        <span style="color: #008800; font-weight: bold">if</span>(x<span style="color: #333333">==</span>sat):
            m <span style="color: #333333">=</span> s<span style="color: #333333">.</span>model()
            <span style="color: #008800; font-weight: bold">for</span> ui <span style="color: #000000; font-weight: bold">in</span> <span style="color: #007020">range</span>(u<span style="color: #333333">+</span>base):
                <span style="color: #008800; font-weight: bold">print</span>()
                <span style="color: #008800; font-weight: bold">for</span> i <span style="color: #000000; font-weight: bold">in</span> <span style="color: #007020">range</span>(n_size):
                    <span style="color: #008800; font-weight: bold">try</span>:
                        <span style="color: #008800; font-weight: bold">print</span>(<span style="background-color: #fff0f0">&quot;node[</span><span style="background-color: #eeeeee">%d</span><span style="background-color: #fff0f0">][</span><span style="background-color: #eeeeee">%i</span><span style="background-color: #fff0f0">] : </span><span style="background-color: #eeeeee">%s</span><span style="background-color: #fff0f0">&quot;</span> <span style="color: #333333">%</span>(ui, i, m<span style="color: #333333">.</span>eval(node[ui][i])))
                    <span style="color: #008800; font-weight: bold">except</span>:
                        <span style="color: #008800; font-weight: bold">pass</span>

attack_graph()
</pre></td></tr></table></div>

